\begin{tabbing}
$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$).
\\[0ex](0 $<$ $\parallel$fpf{-}domain($f$)$\parallel$)
\\[0ex]$\Rightarrow$ ($\exists$\=$g$:$a$:$A$ fp$\rightarrow$ $B$($a$)\+
\\[0ex]$\exists$\=$a$:$A$\+
\\[0ex]$\exists$\=$b$:$B$($a$)\+
\\[0ex]($f$ $\subseteq$ $g$ $\oplus$ $a$ : $b$ \& $g$ $\oplus$ $a$ : $b$ $\subseteq$ $f$
\\[0ex]\& ($\forall$${\it a'}$:$A$. ($\uparrow$${\it a'}$ $\in$ dom($g$)) $\Rightarrow$ ($\neg$(${\it a'}$ = $a$)))
\\[0ex]\& ($\parallel$fpf{-}domain($g$)$\parallel$ $<$ $\parallel$fpf{-}domain($f$)$\parallel$)))
\-\-\-
\end{tabbing}